COMMENT ⊗   VALID 00019 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	TABLE OF CONTENTS
C00006 00003	SECTION 1. Introduction.
C00009 00004	.BEGIN DOUBLE SPACE
C00014 00005	1-II. RUNNING THE EXAMPLES
C00019 00006	RUNNING THE FIRST EXAMPLE.
C00022 00007	RUNNING THE SECOND EXAMPLE.
C00026 00008	RUNNING EXAMPLE THREE.
C00031 00009	.REQUIRE "SYSTEM.PUB" SOURCE_FILE
C00032 00010	SECTION 2.  Bookeeping and Editing Commands.
C00037 00011	2-II. COMMANDS TO EXAMINE THE LIST OF CLAUSES
C00040 00012	2-III.	COMMANDS TO NAME CLAUSES.
C00044 00013	SEt		SE <id> <clauses>
C00046 00014	.REQUIRE "MATCH.PUB" SOURCE_FILE
C00047 00015	SECTION 3. Guiding the Proof and Proof-Checking.
C00048 00016	3-I. COMMANDS FOR PERFORMING RULES OF INFERENCE
C00052 00017	3-II. COMMANDS FOR SUB-PROOFS AND PROOF-CHECKING.
C00057 00018	Example 5.  A simple example of  subproof generation.
C00059 00019	3-II. COMMANDS USEFUL WHEN NO PROOF IS FOUND
C00062 ENDMK
C⊗;
TABLE OF CONTENTS

.BEGIN VERBATIM




Section 1. Introduction..................................... 2
	1-I 	EXAMPLES.................................... 2
	1-II	RUNNING THE EXAMPLES........................ 5
	1-III	GETTING ALONG WITH THE SYSTEM...............11


Section 2. Bookeeping and Editing Commands..................12
	2-I	GENERAL BOOKEEPING COMMANDS.................13
	2-II	COMMANDS TO EXAMINE THE LIST OF CLAUSES.....14
	2-III	COMMANDS TO NAME CLAUSES....................15
	2-IV	SEARCHING AND PATTERN MATCHING..............17
	2-V	PRIMITIVE PATTERN LANGUAGE..................18


Section 3. Guiding the Proof and Proof-Checking.............21
	3-I	COMMANDS FOR PERFORMING RULES OF INFERENCE..21
	3-II	COMMANDS FOR SUB-PROOFS.....................23
	3-III	COMMANDS USEFUL WHEN NO PROOF IS FOUND......26


Section 4. The Language of Strategies.......................27
	4-I	CHOICE STRATEGIES...........................28
	4-II	EDITING STRATEGIES..........................30
	4-III	COMBINING PRIMITIVE STRATEGIES..............31
	4-IV	AUTOMATIC STRATEGY SELECTION................31


Section 5. Theorem Proving Primitives.......................33


Section 6. Question Answering...............................36


Appendix. The BNF Equations for the Prover..................38
	A-I	THE INPUT FORMAT............................38
	A-II	THE STRATEGY LANGUAGE.......................40
	A-III	THE COMMAND LANGUAGE........................41
	A-IV	THE MATCHER.................................43
.END
.NEXT PAGE
SECTION 1. Introduction.
.BEGIN DOUBLE SPACE
1-I. EXAMPLES

Perhaps the easiest introduction
is to follow the development of a few examples.
.END
.BEGIN VERBATIM



EXAMPLE 1.

Consider the following simple problem from propositional calculus:

Given  A(a) ⊃ B, and ¬A(a) ⊃ B, prove B.

This problem could be presented to the prover as:

PRE_PRED: A,B;
PRE_OP: a;
HYPS: A(a)⊃B;
     ¬A(a)⊃B;
THM:  B;
      ;

Or perhaps in a less trivial vein:


EXAMPLE 2.

Consider the following set of statements:

(1)	(∀x∀y)(P(x,y) ∧ P(y,z) ⊃ G(x,z))

(2)	(∀y∃x)(P(x,y))

We might interpret these statements as claiming
	"For all x and y, if x is the parent of y and y is the parent
        of z, then x is the grandparent of z,"
and
	"Everyone has a parent."
.END;


Given these statements as hypotheses we might wish to know if there were individuals x and
 y such that x is the grandparent of y. We could pose that question as the statement:

.BEGIN VERBATIM

(3)	 (∃x∃y)(G(x,y))

.END;


It is  clear that (3) does indeed follow from (1) and (2). How do we  formulate the problem for the 
theorem prover? 

Here is one axiomatization:

.BEGIN VERBATIM

PRE_PRED: P,G; 
VAR:x,y,z;

G1: ∀(x,y)(P(x,y) ∧ P(y,z) ⊃ G(x,z)); 
G2: ∀y∃x P(x,y); 
THM: ∃(x,y)G(x,y); 
;
.END;


.BEGIN DOUBLE SPACE
Some of the conventions displayed in the examples are:

(1) the predicate letters and function symbols must be declared
according to their type.  For example infix and prefix operators are
declared  by INF_OP and PRE_OP respectively. Constants should be declared as
PRE_OPs. 
Similarly infix and prefix predicate
symbols must be declared as INF_PRED and PRE_PRED respectively. 
Propositional letters  should be declared to be prefix predicate symbols.

(2) variables must be declared; the effect of the variable declaration
is to declare the identifier as a variable prefix.  The set of variables is
automatically augmented to include 9 additional `subscripted' variants of each
declared variable.
For example, if x is declared as a variable then  x1,x2,..,x9,
are also  variables and need not be declared.

(3) each statement must be terminated with a semicolon.

(4) statements or sets of statements may be labeled.
These labels can be used to refer to clauses in the on-line editor.  If a statement is labeled, 
THM, then the negation of that statement is formed and is used in the list of input statements.

(5) adjacent like quantifiers may  combined.

(6) the whole set of declarations and input statements must be delimited by a semicolon. 

A complete description of the syntax and semantics of the input format 
is given in the Appendix.

.END 



EXAMPLE 3.


In an investigation of axiomatizations of elementary group theory the following statements
arose:

.BEGIN VERBATIM

(1)	x*x = y*y
(2)	x*(y*y) = x
(3)	x*(y*z) = z*(y*x)
(4)	x*(x*y)  = y
(5)	(x*z)*(y*z) = x*y

.END;

Question: Does (5) follow from (1)-(4)?

The answer is "yes" but it is not immediately obvious.  It is more difficult 
to establish than Example 2.
Notice that this example is a pure equality formulation (i.e., equality is the only
predicate so that all formulas are in fact equations).
This example could be presented to the prover as:

.BEGIN VERBATIM

INF_OP: *;
INF_PRED: =;EQUALITY:=;
VAR: x,y,z;
AXIOMS: x*x = y*y;
	x*(y*y) = x;
	x*(y*z) = z*(y*x);
	x*(x*y) = y;
THM:(x*z)*(y*z) = x*y;
;
.END;

In this example, the name AXIOMS refers the first four statements.

Before presenting a more complicated example, we shall describe how to use the prover
on these first Examples.





.NEXT PAGE

1-II. RUNNING THE EXAMPLES
.BEGIN DOUBLE SPACE

Once the input file has been prepared you are ready to used the theorem prover.
The command: R PROVER, will select the current version of the program.
The appearance of an asterisk (*) signifies that the program is ready.
If you wish the program to make an initial selection of strategies  for your problem
then type: (PROVE DSK: filename). The exact strategies which are chosen are described in
Section 4.
If you would rather  select you own strategies then type: (TRY DSK: filename).
You will then be asked to describe your choice and editing strategies.
See Section 4 for a complete description of strategy selection.

If the (translations of) the set of input statements are found to be inconsistent,
then the sequence of deductions which exhibits that
inconsistency is displayed on the console.  This refutation and the set of strategies
which were employed are also saved on a disk file . The name of the file 
is created from the name of the input file.
Thus, for example, (PROVE DSK: FOO) or (PROVE DSK: (FOO.A)) would create an output
file named N1FOO.PRF. If the  input initially comes for the console using (PROVE) or (TRY), 
then the output file is given the  name, N1PRF.PRF.

It is also possible that the prover terminates without finding a refutation.
This could occur either because the selected strategies do not form a complete set
or because the initial set of clauses is not inconsistent. In either case the program types
NO-PROOF-FOUND and enters the clause editor to wait for commands from the user.

See Section 2 for a description of the the online commands.



.END;



RUNNING THE FIRST EXAMPLE.

The first example is so simple that we shall  just type it in on-line.
The output will then be found on the file N1PRF.PRF.
Material preceeded by | is commentary; statements typed by the user are
preceeded by *.

.BEGIN VERBATIM
*R PROVER 			|retrieve the prover.

*(PROVE)			|The prover is to pick strategies
*PRE_PRED:A,B;			|and input is from the console.
PRE_PRED:A,B;			|Declaration is echoed by prover.
*PRE_OP:a;
PRE_OP:a;
*HYPS: A(a)⊃B;¬A(a)⊃B;
HYPS				|The  statements are echoed.
A(a)⊃B;
¬A(a)⊃B;
*THM:B;				|We wish to prove B.
THM
B;
*;				|This final semicolon signals the end
				|of the input.
HERE-ARE-THE-CLAUSES:		|Here are the translations of the 
				|input statements.
1 A(a)⊃B;
2 B∨A(a);
3 ¬B;				|Notice that the statement of the
				|theorem(THM) has been negated.
4 A(a);				|The first deduction.
5 ¬A(a);			|Another deduction.
COUNT 3
LEVEL 1				|These are statistics printed by the 
ELAPSED-TIME 134		|prover. Time is in milliseconds.
6 B;
COUNT 5
LEVEL 2				|The end of level-2 deductions.
ELAPSED-TIME 288
.GROUP
				|A proof  has been found.
				|NIL is our representation for
				|contradiction.
NIL 1 6				|Here's a proof-tree:
1 B; 3 4			|  6    5
3 A(a); 5 6			|   \  /
4 A(a)⊃B; HYPS			|    3    4
5 B∨A(a); HYPS			|     \  /
6 ¬B; THM			|       1    6
*				|        \  /
				|         NIL
.APART
.END
Notes:
.NARROW 8
1. Though all statements are stored internally in conjunctive normal form,
an attempt is made to improve the readibility on output. Clauses are translated
for output as follows:

a)clauses containing only positive literals appear as a disjunction.

b)clauses containing only negative literals appear as the negation of
a conjunction.

c)mixed clauses, containing positive and negative literals appear in the
form of an implication.




.WIDEN
RUNNING THE SECOND EXAMPLE.



Assume that a disk file, EX2, has been prepared
containing the axiomatization. What follows is a running commentary on what should 
occur.

.BEGIN VERBATIM

*R PROVER 			|retrieve the current prover.

*(PROVE DSK: EX2)		|Request that the program pick the
				|strategies while running EX2.
PRE_PRED: P,G;			|The program is accepting the axioms.
VAR: x,y,z;
G1:
∀(x,y)(P(x,y) ∧ P(y,z)) ⊃ G(x,z));
G2:
∀y∃x P(x,y);
THM:
∃(x,y)G(x,y);

HERE-ARE-THE-CLAUSES:		|What follows are the translations 
				|of the input into clause-form.
1 P(x,z)∧P(y,z) ⊃ G(x,y)    	|
2 P(G21(x),x)  			|G21 is a generated Skolem function.
3 ¬G(x,y)			|The translation of the negation of 
				|the theorem.

4 ¬(P(z,x)∧P(x,y)) 		|A deduction which has been added to 
				|the list of clauses.
COUNT = 1			|There was only one resolvent formed
LEVEL = 1			|on level one.
ELAPSED-TIME = 333		|The execution time in milliseconds.

.GROUP
5 ¬P(x,y);

COUNT = 3
LEVEL = 2			|Three resolvents have been formed by
ELAPSED-TIME = 500		|the end of level 2. (Two have been 
				|retained.)
NIL 1 4				|A contradiction. These next six 
1 ¬P(x,y) 3 4			|lines are the refutation. I.e.:
3 ¬(P(z,x)∧P(x,y)) 5 6	 	|  6    5
4 P(G21(x),x) G2	     	|   \  /
5 P(x,z)∧P(y,z) ⊃ G(x,y) G1	|     3     4
6 ¬G(x,y) THM			|       \  /
				|         1    4
				|          \  /
				|            NIL


.APART
.END;
.GROUP
Notes: 
.NARROW 8;

1. A copy of the refutation tree, relevant statistics, and  a description of the
actual strategies used, now appears on a file named N1EX2.PRF.




.WIDEN
.APART

RUNNING EXAMPLE THREE.



Assume that the axiomatization is on a file named
 EX3.

.BEGIN VERBATIM 

*R PROVER

*(PROVE DSK: EX3)		|Again, let the program
				|pick the strategies.
INF_OP: *;
INF_PRED: =;
EQUALITY: =;
VAR:x,y,z;
AXIOMS:
x*x=y*y;
x*(y*y)=x;
x*(y*z)=z*(y*x);
x*(x*y)=y;
THM:
(x*z)*(y*z)=x*y;

HERE-ARE-THE-CLAUSES:

1 x*x=y*y 
2 x*(y*y)=x
3 x*(y*z)=z*(y*x)
4 x*(x*y)=y
¬(THM1*THM3)*(THM2*THM3)=THM1*THM2
				|Again, THMn's are generated
				|Skolem constants.

NIL 1 2				|An immediate contradiction
1 x=x;			     	|We know = is reflexive
2 ¬THM1*THM2=THM1*THM2;	 3 4 	|moderate mystery.
3 x*(y*z)=z*(y*x); AXIOMS
4 ¬(THM1*THM3)*(THM2*THM3)=THM1*THM2; THM
.END;

Notes:



1. The `refutation' is a bit mysterious.  A more sympathetic proof recovery
mechanism is contemplated, but perhaps some of the current mystery can be dispelled.

A `natural' proof might be:

.BEGIN VERBATIM
	I.  (x*z)*(y*z) = z*(y*(x*z))  replacement in THM 
					using CLAUSE 3.
	II. z*(y*(x*z)) = z*(z*(x*y))  replacement in I 
					using CLAUSE 3.
	III.z*(z*(x*y)) = x*y          replacement in II 
					using CLAUSE 4	.
.END;

.BEGIN DOUBLE SPACE
The above proof is indeed a translation of the machine proof.
See the proof tree below.

The proof is generated using the following rule: Besides replacement,
the prover also has a special rule of simplification. Whenever an equality
formulation is presented to the prover a list is made consisting
 of all the equalities which occur in the input.
In the current example, this list would consist of everything but the negation of the 
theorem. Let  t1=t2 be a member of the list. Whenever a deduction is formed  (but before
it has been added to the memory of the prover) we attempt to match t1 against terms
occurring in the deduction. If matches can be made we replace those terms with the
appropriate instance of t2. It is this simplified deduction which is presented to the
editing strategies of the prover.

.END;



.GROUP

Thus the refutation really is:
.BEGIN VERBATIM

¬(THM1*THM3)*(THM2*THM3)=THM1*THM2  THM
	\
	  \
	    \  x*(y*z)=z*(y*x) AXIOMS
	      \      /
		\  /
¬THM3*(THM2*(THM1*THM3))=THM1*THM2  by replacement 
		\        
	  	  \
		    \ x*(y*z)=z*(y*x)  AXIOMS
		      \       /
			\   /
¬THM3*(THM3*(THM1*THM2))=THM1*THM2  by simplification 
		\	
		  \
		    \ x*(x*y)=y  AXIOMS
		      \       /
			\   /
         ¬THM1*THM2=THM1*THM2  by simplification 
 	       \ 
		 \
		   \          x=x
		     \        /
		       \    /
			NIL
				by resolution
.END;
.APART


.NEXT PAGE

.REQUIRE "SYSTEM.PUB" SOURCE_FILE
.NEXT PAGE 
SECTION 2.  Bookeeping and Editing Commands.
.SKIP 3
.BEGIN DOUBLE SPACE
Most applications of the prover lie in that gray area between a quick proof and the occurrence of 
NO-PROOF.  That is, an application of the prover usually generates a large number
of deductions before either a proof is found or no more deductions can be made
under the current strategy settings.
It is this area which can be profitably explored using interactive commands.
If the user sees a deduction which  should lead to the desired  refutation
he is able to guide the program to the explicit contradiction.  If he sees
a deduction which he feels is interesting, he can explore its consequences in the
set of statements.  If he feels that the strategy settings are ill-chosen
then he can abandon the current proof-search and pick new strategies.  The next
sections give detailed descriptions of the current on-line commands.

All of the commands may be abbreviated to their first two  letters.

First, the on-line editor is entered by striking the space bar.

.END;
.NEXT PAGE
2-I. GENERAL BOOKEEPING COMMANDS.

CHange		CH;
.NARROW 16;
It is  frequently desirable to change some of the strategies while a proof attempt is in progress.
CHange describes what choice and editing strategies are currently active and 
asks which are to be changed.  If a change is desired type YES(or Y) and follow with
the desired strategy; if no change is needed, type NO(N).
.WIDEN;

COntinue	CO;
.NARROW 16;
This command is used to exit from the on-line editor and continue the
interrupted  proof search.
.WIDEN;

CUrrent		CU;
.NARROW 16;
This command simply lists the current strategy settings.
.WIDEN;

DSkout		DS <filename>;
.NARROW 16;
This command diverts future output to the specified disk file. 
Use the EOf command to  terminate the DSkout command.
.WIDEN;

EVal	 	EV;
.NARROW 16;
This command is  mostly a debugging aid and is included for completeness.  The casual users should not have to resort
to its use.  EVal enters a READ-EVAL-PRINT loop. To return to the editor, type @END.
.WIDEN;

HAlt		HA;
.NARROW 16;
HAlt stops the prover in such a state that if the current core image is saved, it can
be continued.  To  resume execution of such a core image, type RUN  DSK: name.  When the
asterisk appears you are in the on-line editor. Then type COntinue.
.WIDEN;

End Of file	EO;
.NARROW 16;
EOf is used to terminate the DSkout command.

.WIDEN;
HElp		HE;
.NARROW 16;
This command will type a list of the available editing commands along with an abbreviated description of their action.
.WIDEN;


.SKIP 3
2-II. COMMANDS TO EXAMINE THE LIST OF CLAUSES
.SKIP 3
.BEGIN DOUBLE SPACE
Each  clause which has been retained by the prover -- initial clause or 
deduction -- is given a number, the first axiom, the
number 1., etc.. These numbers are permanently assigned, even though certain
actions of the prover may delete  clauses from active status (in which case they are
not used in making  any future deductions).
Clauses which have been so deleted are displayed as *DE*.  When the editor is entered,
an invisible pointer is initialized to the first clause.  This first  set of commands
allow the user to manipulate the set of clauses using the pointer or the numbers associated
with the clauses.

.END;

FLoat UP	FU; or FL UP;
.NARROW 16 ;
Moves the pointer up through the clause list displaying each clause.  The motion is stopped
either by striking a key or by reaching the upper extreme of the
list. FLoat UP may also be apbbreviated as FU.
.WIDEN;

FLoat DOwn	FD; or FL DO;
.NARROW 16;
The counterpart of FLoat UP. FLoat Down may also be abbreviated 
as FD.
.WIDEN;

UP		UP n;
.NARROW 16;
UP is followed by an integer, n.  The effect of this command
is to move the pointer up n clauses from its current  setting. As the pointer
is moved, the interviening clauses are printed.
If n = 0, then the pointer is immediately moved to the beginning of the 
clause list.  As with the FLoat commands, striking a key will stop the pointer.
.WIDEN;

DOwn		DO n;
.NARROW 16;
The counterpart of UP. DOwn 0 moves the pointer to the end of
the list.
.WIDEN;

GO		GO n;
.NARROW 16;
GO is followed by an integer designating a clause.  The pointer goes  
immediately to the designated clause and the clause is printed.
.WIDEN;



.SKIP 3
2-III.	COMMANDS TO NAME CLAUSES.
.SKIP 3
.BEGIN DOUBLE SPACE
Though the previously described commands  have proved quite useful, experience  has shown that more
global manipulation of the clauses is needed. Therefore we have developed commands for
assigning names to subsets of the clause list, and commands for manipulating these sets.

Some sets of clauses are assigned names automatically by the prover.  The main clause
list is named CLAUSES; and the simplification list for the equality rule (see
Example 3, Section 1-I)is named DLIST.  Also if any of the input statements were
named in the input file those names will be present in the symbol table.  Input
statements which were not named by the user can found under the name, AXIOMS.

Just as each element of the primary list of clauses is assigned a unique positive integer,
so is each element of each named subset.  For example to refer to the second element of the
set  named FOO, use FOO[2]; to refer to the second and third elements, use FOO[2,3].

Clauses may thus be referenced explicitly by their number in the main clause list
or by their position in a named set.(For example, the n-th clause is also CLAUSES[n].)
Clauses may also be referenced implicitly through the pattern matcher.  See Section 2-IV.

To be more precise about the nature of clauses, the following BNF equations will be used in the sequel:
 
.END;
.BEGIN VERBATIM;

<clauses> ::= {<c>,}*<c>

<c>	  ::= <number>|<id>{[{<number>,}*<number>]}*

	  ::= @<statment>|FIND[<id>;<pattern>]|FINDC[<pattern>]

.END;

ADd		ADd <clauses>;
.NARROW 16;
Most of the results of the on-line commands: deductions, insertions,
substitutions, etc., are local to the clause editor.  To include any of
these resulting clauses in the memory of the prover use the ADd command.
.WIDEN

ANcestry	AN <clauses>;
.NARROW 16;
The ancestry command is used to display the derivation tree of the specified clauses.
.WIDEN
CLear		CL <id>;	
.NARROW 16;
CLear takes a name as argument. This command only removes the
name from the symbol table; it does not affect the clauses attached to the
name.
.WIDEN;

DElete		DE <clauses>;
.NARROW 16;
The designated clauses are deleted from the memory of the prover. Attempts to display
 such clauses will print *DE*.  Other attempts to use deleted clauses in editing commands
will  invoke an error message.
.WIDEN;

DIsplay		DI <clauses>;
.NARROW 16;
This command displays all the elements of <clauses>.
.WIDEN;



SEt		SE <id> <clauses>;
.NARROW 16;
SEt <id> <clauses>; has the effect of assigning
to <id> the sequence of clauses selected by the <clauses>.
Within a particular proof attempt, the names selected by the user are retained.
.WIDEN;

SUbstitute	SU <term>; FOR <term>; IN <clauses>;
.NARROW 16;
The effect of the SUbstitute command is to substitute the first <term> for
every occurrence of the second <term> in copies of all of the designated <clauses>.
Notice that the original <clauses> are kept intact. The modified  <clauses>
are added to the list named ASSERT.
.WIDEN

SYmbols		SY;
.NARROW 16;
Display the current symbol table of clause names.
.WIDEN

.SKIP 3
.REQUIRE "MATCH.PUB" SOURCE_FILE
.NEXT PAGE
SECTION 3. Guiding the Proof and Proof-Checking.
.SKIP 3
.BEGIN DOUBLE SPACE
The commands listed above give us a reasonably powerful set of instructions for
manipulating the clause list. Clearly, before we can really begin to guide the prover
we must be able to perform the rules of inference on-line. The next  set of commands
begins to do this.


.END;



3-I. COMMANDS FOR PERFORMING RULES OF INFERENCE



PAramodulate		PA <clauses>; <clauses>;
.NARROW 16;
This command handles equality replacements.
All equality literals of the form t1=t2, are used in equality replacements in the following manner:
let t1=t2 be an equality literal occurring in a clause of one of the <clauses>;
let s be any term, not a variable, which occurs in some literal in the other <clauses>.
If s occurs no deeper than PDEPTH (see Section 4-I. for PDEPTH) and there is a substitution
 unifying s and t1, then the occurrence of s is replaced by the appropriate instantiation
of t2.  The paramodulants are assigned a new name of the form PARn.  See the REsolve
command.
.WIDEN;

REsolve			RE <clauses>;<clauses>;
.NARROW 16;
This command takes a pair of <clauses> as arguments.  The resolvents of these
two sets are formed, a unique name is generated and the resolvents are assigned to that
new name.  The generated names are presently of the form RESn, for some integer,n.
The created names, PARn and RESn are only local names, that is, returning to the
prover (via COntinue) will destroy them.  Use the ADd command to save desired
computations.
.WIDEN;

SImplify		SImplify <clauses>; BY <clauses>;
.NARROW 16;
This command is similar to the PA command.  Here the second set of clauses is to be a
list of equality units, again of the form t1=t2. Terms occuring in the first set of clauses
which unify with elements, t1, are replaced by instances of t2.  DDEPTH determines the
depth to which the match is attempted.
.WIDEN;

Example 4.  A simple example of the use of the rules of inference.

Assume that = is the equality predicate and that we have just struck a key on the
console.

.BEGIN VERBATIM


*DI 1,2,3;			|Display the first three clauses
1 x≤y ⊃ x/y=0
2 ¬1/(a/b)=0
3 0≤x

*PA 1; 2;			|Use replacement on 1 and 2.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME: PAR1	|PAR1 is a created name.

1 1≤a/b ⊃ 1=0

*PA 2; 3;			|Try to use the replacement rule
NO-PARAMODULANTS		|on clauses 2, and 3.

*RE 1; 3;
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:RES1	|RES1 is another created
				|name.
1 0/x=0

*PA RES1; RES1;			|Created names are legal.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:PAR2	|PAR2 is a new name.

1 0=0				|True.

*AD PAR1[1];			|Add 1≤a/b ⊃ 1=0 to the memory
				|of the prover.

.END;

.NEXT PAGE


3-II. COMMANDS FOR SUB-PROOFS AND PROOF-CHECKING.

.BEGIN DOUBLE SPACE
Though the commands, REsolve and PAramodulate, are useful for fine control of the
prover, it is often useful to demand larger inference steps. That is, using some of the
existing clauses in memory, with perhaps some additional assumptions, we wish the
prover to attempt to establish the validity of a  first order formula. While this
subproof is  under investigation the state of the main proof should be preserved.
The commands in this section are used to initiate and control such subproofs.

.END;


ABandon		AB ; or AB <clauses>;

.NARROW 16;
This command is used to abandon a proof attempt, returning the prover to the previously
 saved state.
If <clauses> is present, then the selected clauses are returned and assigned
to a created name.
.WIDEN;


USing		US <clauses>; 
.NARROW 16;
The selected clauses are designated to be used in the forthcoming
subproof.
.WIDEN;

PRove		PR <statement>;
.NARROW 16;
The <statement> is translated and will be attached to the name LEMMA. The negation 
of the statement is also formed and will be used in the subproof. Thus both the positive and negative 
translates are formed.  The positive translate is maintained for the convenience of the
user since after the lemma has been established  it  should be available for further 
deductions.  Within the subproof the negation of the <statement> will appear under the local
name, THMS.
.WIDEN;

These last two commands --USing, and PRove -- are used to initialize the call
on the prover; USing may be omitted. There are two  commands to
commence the subproof.

EXecute		EX;
.NARROW 16;
EXecute begins the subproof using a computed set of stategies.
.WIDEN;

TRy		TR;
.NARROW 16;
TRy first enters the strategy selection dialog, then begins the subproof with the chosen strategies.
.WIDEN;

In both cases the strategies of the subproof are completely local.  They in no way
affect the strategies in the parent proof. If a key is struck while in the subproof,
the editor is entered and can manipulate the local clauselist or initiate another
subproof. The Continue command will continue the subproof, the ABandon command will
return to the previous subproof level.


.NEXT PAGE

Example 5.  A simple example of  subproof generation.

Suppose that we have struck a key during a proof-search.
.BEGIN VERBATIM

*AN 10;				|Display the ancestry of 
P(A) 1 2			|clause no. 10.
1 P(A) ∨ P(B)  AX1
2 ¬P(B)	     HYP1

*USING 10, @P(A) ⊃ P(B); ;	|Setup the assumptions for the
				|lemma.
				|Use clause no. 10 in the attempt

*PROVE @P(B);;

*EX;				|This initiates the subproof.

NIL 1 2
1 P(A) DEDUCT			|Clause 10 becomes an "axiom"
2 ¬P(A)	3 4			|within the subproof.
3 P(A)⊃P(B)  INSERT 
4 ¬P(B) THM	 		|The negation of the lemma

PROOF-FOUND-FOR-LEMMA
				|We are now back in the  editor
*DI 10;				|Display clause no. 10.
P(A)

*DI LEMMA;			|The translate of the statement 
P(B)				|to be PROVEed.

*USING LEMMA;

*PROVE @∃(x)P(x);;		|LEMMA now becomes the translate
*EX;				|this clause.
NIL 1 2
1 P(B) AX1
2 ¬P(X1) THM

PROOF-FOUND-FOR-LEMMA

*DI LEMMA;			|ED1 is a ubiquitous Skolem 
P(ED1)				|constant.
.END;

.NEXT PAGE



3-II. COMMANDS USEFUL WHEN NO PROOF IS FOUND

.BEGIN DOUBLE SPACE;

When the prover is unable to make new deductions which satisfy the current
strategies it will report that no refutation can be found, and will enter
the on-line editor. At this time  the user can examine the list of clauses,
perform rules of inference, initiate sub-proofs,
save any or all of the current deductions
and begin the proof search again, perhaps with new strategies.
The user can also force a proof attempt to be abandoned by typing AB;.  This
has exactly the same effect as if the prover could make no new deductions.

.END;

ABandon		AB;

.NARROW 16
AB, typed in this context (not in a subproof) terminates the main proof attempt,
enters the on-line editor, and waits for commands.
.WIDEN

TErminate	TE <clauses>; or TE;

.NARROW 16
If <clauses> are present then they are added to the list of clauses named THMS.
The list of initial clauses is preserved and a new proof attempt is begun.
If the initial attempt was through PROVE then the user is asked if he still wants
automatic strategy selection.  If the initial attempt was through TRY or the
user does not wish automatic selection, then a dialogue is begun describing the
current strategies and asking if changes are desired.
Then a new proof search is begun.
.WIDEN

.BEGIN DOUBLE SPACE

This use of AB and TE is useful for feeding `interesting' deductions back into a
proof search without having to restart the whole process.  The derivation tree
of any such saved derived clause is maintained for the proof recovery mechanisms
but such clauses appear to be `input' clauses to the rules of inference.

.END;